Problem:
 f(g(x),s(0()),y) -> f(g(s(0())),y,g(x))
 g(s(x)) -> s(g(x))
 g(0()) -> 0()

Proof:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {4,3}
   transitions:
    01() -> 5,4
    s1(5) -> 5,4
    g1(2) -> 5*
    g1(1) -> 5*
    f0(1,1,1) -> 3*
    f0(2,2,1) -> 3*
    f0(1,1,2) -> 3*
    f0(2,2,2) -> 3*
    f0(1,2,1) -> 3*
    f0(2,1,1) -> 3*
    f0(1,2,2) -> 3*
    f0(2,1,2) -> 3*
    g0(2) -> 4*
    g0(1) -> 4*
    s0(2) -> 1*
    s0(1) -> 1*
    00() -> 2*
  problem:
   
  Qed